COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	INTRODUCTION
C00013 00003	outline	
C00014 ENDMK
C⊗;
INTRODUCTION

	This text offers the student the opportunity to learn two
skills.  The first is programming in LISP, a programming language
that emphasizes a different way of thinking about programs than
does machine language or languages like Algol, Fortran or Pascal
and which is extensively used for computing with mathematical
expressions and in artificial intelligence.
The second skill is in proving that programs meet their specifications.


RECURSIVE PROGRAMMING IN LISP

	The book is self-contained, although most students who take a course
in LISP have had previous experience or course work in programming.
This experience is normally with sequential programming languages
wherein a program is a collection of statements, each of which
alters the state of the computation.  The programmer's task is to
write a program that will take an initial state into a desired state
in which certain variables have as values the "answers" to the problem
being solved.

	While sequential programming is available in LISP and has important
applications, we emphasize mainly recursive programming
using conditional expressions.  A program is a collection of mutually
recursive function definitions, and the programmer's goal is a function that
gives the "answer" in terms of initial data.

	As a programming language, LISP is characterized by the following
ideas:  computing with symbolic expressions rather than numbers,
representation of symbolic expressions and other information by list
structure in the memory of a computer,
representation of information in external media mostly by multi-level lists and
sometimes by S-expressions,
a small set of selector and constructor
operations expressed as functions,
composition of functions as a tool for
forming more complex functions,
the use of conditional expressions for
getting branching into function definitions,
the recursive use of
conditional expressions as a sufficient tool for building computable
functions,
the use of λ-expressions for naming functions,
the representation of LISP programs as LISP data,
the conditional expression interpretation of Boolean connectives,
the LISP function %2eval%1 that
serves both as a formal definition of the language and as an interpreter,
and
garbage collection as a means of handling the erasure problem.
LISP statements are also used as a command language when LISP is used
in a time-sharing environment.  Since LISP programs are LISP data,
is is easy to make programs that produce other programs.  Powerful
macros are particularly easy to write in LISP.


PROOFS OF PROGRAM CORRECTNESS

	We believe that proving that programs meet their specifications is
the very core making a mathematical computer science that is connected
with its applications.  We also believe that proving the correctness of
programs will soon be practical - to the extent that no-one will pay money
for a program without a computer checked proof that the program meets its
specifications.

	We can't yet require a correctness proof for all programs assigned
as exercises in the book.  Part of the reason is that the proof techniques
do not cover all the programming techniques we shall present.  Moreover,
making the correctness proof is several times the work of writing the
program - though not necessarily more work than debugging a misconceived
or sloppily written program.  Nevertheless, the techniques are good enough
and easy enough so that it has been possible to include problems of the
form %2Write a program to do X and prove that it does it%1 on final
examinations at Stanford and get a majority of substantially correct
solutions.

	Correctness proofs should also improve the logical clarity and
understandability of programs, since such a program will be easier to
prove correct than an original patched together version.  Since proving
involves the content of the program as well as the form, this should be
more effective in assuring good programs than purely syntactic structural
rules like the infamous ban on %3go_to%1s.

	There are two main lines of research in program proving today.
The first was mentioned in passing by both Turing and von Neumann, but its
systematic treatment begins with Floyd (1967) and continues with the work
of Hoare, Dijkstra and many others.  It involves attaching declarative
statements to points in a program and proving that if the statement
attached to one point is true, the statement attached to succeeding points
will also be true.  Usually this %2inductive assertion%1 method and its
variants lead to partial correctness proofs, i.e. it is proved that if the
inputs to a program meet certain conditions, then the outputs will meet
certain other conditions provided the program terminates - which usually
must be proved separately.

	The second line of research treats programs as functions and
begins with (McCarthy 1963) and continues with the work of Scott and
others.  While its systematic study began earlier than that of the
%2inductive assertion%1 method, it assumed a very practical form with the
work of Cartwright (1976) who showed how to represent the LISP programs
themselves as functions in first order logic.  The work of Boyer and Moore
(197x) in proving partial correctness of LISP programs was already similar
in spirit and was immediately adaptable to proving total correctness.

	There is little doubt that functional methods of proving programs
correct are more appropriate for LISP than %2inductive assertions%1 or its
"dual" introduced by Manna and Pnueli (19xx) and named %2subgoal
induction%1 by Morris and Wegbreit (197x).  However, they have advantages
over the input-output relation methods for even for sequential programs.
Namely, they allow proving algebraic assertions that cannot even be
asserted as input-output relations.  An example is the assertion that the
operation %2u*v%1 of concatenating two lists ⊗u and ⊗v is associative,
i.e.  %2u*(v*w)_=_(u*v)*w%1 and that it is related to the operation of
reversing a list by %2reverse(u*v)_=_reverse(v)*reverse(u)%1.
Representing the programs themselves as sentences and sentence schemata in
first order logic makes for a compact notation that can be quickly learned
and promptly applied by advanced undergraduates and beginning graduate
students.  When we have learned more about teaching it, it may be usable
even by beginning college students.

	We have experimented with computer checked proofs of correctness
of LISP programs using the FOL first order logic proof checker developed
by Richard Weyhrauch.  The proofs go well and are reasonably compact, but
the present version of FOL takes too much computer time and has too many
conventions that have to be learned.  Most likely, we shall need a
proof checker closely integrated with the LISP system itself.
outline	

general purpose

two tendencies in program proving

what kind of a programming language is LISP

omissions in this edition